T:Type, eq:EqDecider(T), f, g, h:x:T fp Type.
f || g
 h || f
 h || g
 {g  h  f  g & f  h  f  g & h  g  h  f  g & h  f  h  f  g} 

latex

Definitions	f  g, A & B, if b t else f fi, Unit, , b, P  Q, P  Q, P & Q, f  g, Top, x  dom(f), f(x), A, False, Prop, P  Q, b, P  Q, {T}, f || g, a:A fp B(a), x. t(x), EqDecider(T), x:A. B(x), t  T
Lemmas	deq wf, fpf wf, fpf-compatible wf, assert wf, fpf-dom wf, fpf-join wf, fpf-trivial-subtype-top, fpf-join-dom2, or functionality wrt iff, iff transitivity, not wf, bnot wf, fpf-ap wf, assert of bnot, eqff to assert, eqtt to assert, bool wf, fpf-join-ap-sq, top wf